home *** CD-ROM | disk | FTP | other *** search
/ Amiga Tools 2 / Amiga Tools 2.iso / tex / macros / source / contrib / vdm / vdm.sty next >
Encoding:
Text File  |  1995-03-10  |  38.4 KB  |  1,186 lines
  1. %%% ====================================================================
  2. %%%  @LaTeX-style-file{
  3. %%%     author          = "Mario Wolczko",
  4. %%%     version         = "4.00",
  5. %%%     date            = "14 October 1994",
  6. %%%     filename        = "vdm.sty",
  7. %%%     address         = "FORMERLY AT
  8. %%%                        Dept of Computer Science
  9. %%%                        The University of Manchester
  10. %%%                        Oxford Road
  11. %%%                        Manchester M13 9PL
  12. %%%                        UK",
  13. %%%     codetable       = "ISO/ASCII",
  14. %%%     keywords        = "LaTeX, VDM specification language",
  15. %%%     supported       = "yes",
  16. %%%     docstring       = "LaTeX macros for typesetting VDM
  17. %%%                        specifications.
  18. %%%                        NOTE
  19. %%%                        Mario no longer works at Manchester
  20. %%%                        This is a minimal update to LaTeX2e
  21. %%%                        By David Carlisle",
  22. %%%  }
  23. %%% ====================================================================
  24. %
  25. %       BSI VDM documentstyle option for LaTeX
  26. %
  27. %       M. Wolczko
  28. %
  29. %
  30. % Dept. of Computer Science   Internet:      mario@cs.man.ac.uk
  31. % The University              uucp:    mcsun!uknet!man.cs!mario
  32. % Manchester M13 9PL          JANET:         mario@uk.ac.man.cs
  33. % U.K.                        Tel: +44-61-275 6146  (FAX: 6236)
  34. %
  35. % Version for LaTeX2e by David Carlisle.
  36. % Just constructed by removing all the old font wierdness.
  37. % Not tested at all!
  38. %
  39. %
  40. %----------------------------------------------------------------
  41. %
  42. %       Installation-dependent features
  43. %
  44.  
  45.  
  46. \newif\ifams@ 
  47.  
  48. \ams@true
  49.  
  50. \ifams@
  51.  \RequirePackage{amsfonts}
  52. \fi
  53.  
  54. %----------------------------------------------------------------
  55. %
  56. %       The vdm environment
  57. %
  58. % record whether we were in horizontal mode when entering...
  59. \newif\ifhm@
  60.  
  61. \def\vdm{\ifhmode\hm@true\else\hm@false\fi
  62.   \@changeMathmodeCatcodes\@postUnderPenalty10000\relax}
  63.  
  64. % after an \end{vdm} the next paragraph is not indented unless a \par
  65. % comes first (if we entered in horizontal mode).  This is a bit of a
  66. % kludge!
  67. \def\endvdm{\ifhm@\else
  68.   \global\let\par=\@undonoindent
  69.   \global\everypar={{\setbox0=\lastbox}\global\everypar={}%
  70.                         \global\let\par=\@@par}%
  71.   \fi}
  72.  
  73. \def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}
  74.  
  75. %-----------------------------------------------------------------
  76. %
  77. %       Controlling line and page breaks
  78. %
  79. % Text within the vdm environment is essentially mathematical in
  80. % nature, so requires special care.  Whenever outer vertical mode is
  81. % entered, the \@beginVerticalVDM command should be used.  This sets
  82. % up \leftskip, \rightskip, \baselineskip, \lineskip and
  83. % \lineskiplimit to conform with the overall style.
  84. %
  85. % When entering unrestricted horizontal mode, the \@beginHorizontalVDM
  86. % command should be used.  This sets up:
  87. %       \leftskip and \rightskip to 0,
  88. %       \\ to do line breaking
  89. %       ragged right line breaking, with special penalties, and
  90. %       enters math mode.
  91. % \@endHorizontalVDM should be called when leaving unrestricted
  92. % horizontal mode.
  93.  
  94. \def\@beginVerticalVDM{\@changeMargins\@changeBaselineskip}
  95.  
  96. \def\@beginHorizontalVDM{\@restoreLineSeparator
  97.   \@restoreMargins\@raggedRight\noindent$\strut\relax}
  98. \def\@endHorizontalVDM{\relax\strut$}
  99.  
  100. % \VDMindent is used for \leftskip within VDM, \VDMrindent for
  101. % \rightskip, \VDMbaselineskip for \baselineskip
  102. \newdimen\VDMindent \VDMindent=\parindent
  103. \newdimen\VDMrindent \VDMrindent=\parindent
  104. \def\VDMbaselineskip{\baselineskip}
  105.  
  106. \def\@changeMargins{\leftskip=\VDMindent \rightskip=\VDMrindent}
  107. \def\@restoreMargins{\advance\hsize by-\leftskip
  108.   \advance\hsize by-\rightskip
  109.   \leftskip=0pt \rightskip=0pt}
  110. \def\@changeBaselineskip{\baselineskip=\VDMbaselineskip
  111.   \lineskip=0pt \lineskiplimit=0pt
  112.   % need to alter the size of struts, too
  113.   \setbox\strutbox\hbox{\vrule height.7\baselineskip
  114.       depth.3\baselineskip width\z@}}
  115.  
  116. % these are used in externals, records and cases
  117. \def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
  118. \def\@restoreLineSeparator{\let\\=\newline}
  119.  
  120. \def\@raggedRight{\rightskip=0pt plus 1fil
  121.   \hyphenpenalty=-100 \linepenalty=200
  122.   \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
  123.  
  124. % ------------------------------------------------------------------------
  125.  
  126. %       Font and Character Changes
  127.  
  128. % make a-zA-Z use the \it family within math mode, and ~ mean \hook.
  129. % Digits 0-9 remain as normal.
  130. \everymath=\expandafter{\the\everymath\vdm@it
  131.         \@changeMathmodeCatcodes}%
  132. \everydisplay=\expandafter{\the\everydisplay\vdm@it
  133.         \@changeMathmodeCatcodes}%
  134.  
  135. \def\vdm@it{\@fontswitch\it\mathit}
  136.  
  137. \mathcode`\0="0030
  138. \mathcode`\1="0031
  139. \mathcode`\2="0032
  140. \mathcode`\3="0033
  141. \mathcode`\4="0034
  142. \mathcode`\5="0035
  143. \mathcode`\6="0036
  144. \mathcode`\7="0037
  145. \mathcode`\8="0038
  146. \mathcode`\9="0039
  147.  
  148. \mathchardef\Gamma="0000
  149. \mathchardef\Delta="0001
  150. \mathchardef\Theta="0002
  151. \mathchardef\Lambda="0003
  152. \mathchardef\Xi="0004
  153. \mathchardef\Pi="0005
  154. \mathchardef\Sigma="0006
  155. \mathchardef\Upsilon="0007
  156. \mathchardef\Phi="0008
  157. \mathchardef\Psi="0009
  158. \mathchardef\Omega="000A
  159.  
  160. % If the user really wants the normal codes, she can call \defaultMathcodes
  161. %\def\defaultMathcodes{\let\vdm@it\relax}
  162. \def\defaultMathcodes{\let\vdm@it\relax}
  163.  
  164.  
  165. % remember the original mathcode of minus sign
  166. \edef\@minuscode{\the\mathcode`\-}
  167.  
  168. \def\mathminus{\mathcode`\-=\@minuscode }
  169. \def\textminus{\mathcode`\-="002D }
  170. % by default, use text minus
  171. %\textminus
  172.  
  173. % make a : into punctuation, a - into a letter, and | mean \mid
  174.  % NFSS-change
  175.  % \mathcode`\-="042D changed to \mathcode`\-="002D as we can not rely on
  176.  % \itfam being fam 4.
  177.  \def\@changeOtherMathcodes{\mathcode`\:="603A \textminus
  178.   \mathcode`\|="326A \mathchardef\Or="325F }% this is a rel to get 5mu spacing
  179.  \def\relbar{\mathrel{\smash\minus}}% redefine because mathcode of -
  180.                                     % has changed
  181.  
  182.  
  183. % alternative underscore
  184. \def\@VDMunderscore{\leavevmode
  185.   \kern.06em\vbox{\hrule\@height .2ex\@width .3em}\penalty\@postUnderPenalty
  186.   \hskip 0.1em}
  187.  
  188. % Allow line breaks after an underscore, but not in vdm mode (see
  189. % \vdm).  This is so long identifiers can be broken when run
  190. % into paragraphs.
  191. \newcount\@postUnderPenalty \@postUnderPenalty=200
  192.  
  193. % now require some catcode trickery to enable us to change _ when we want to
  194. {\catcode`\_=\active 
  195.  \gdef\@changeGlobalCatcodes{% make _ a normal char
  196.         \catcode`\_=\active \let_=\@VDMunderscore}
  197.  \gdef\@changeMathmodeCatcodes{%
  198.         % make ~ mean \hook, " do text, @ mean subscript
  199.         \let~=\hook
  200.         \catcode`\@=8
  201.         \mathcode`\"="8000 }
  202.         \uccode`\~=`\"%
  203.  \gdef\underscoreoff{% make _ a normal char
  204.         \catcode`\_=\active \let_=\@VDMunderscore}
  205.  \gdef\underscoreon{% restore underscore to usual meaning
  206.         \catcode`\_=8}
  207. \uppercase{\gdef~}#1"{\nfss@text{\rm #1}}}
  208.  
  209. %----------------------------------------------------------------
  210. %
  211. %       Keywords
  212. %
  213. \ifx\fmtname\@fmtname
  214.         \def\keywordFontBeginSequence{\sf}%     user-definable
  215. \else\ifx\fmtname\@psfmtname
  216.         \def\keywordFontBeginSequence{\sf}% Helvetica is OK
  217. \else
  218.         \def\keywordFontBeginSequence{\bf}% good for SliTeX
  219. \fi\fi
  220.  
  221. \def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
  222.  
  223. \def\makeNewKeyword#1#2{% use \newcommand for extra checks
  224.         \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}
  225.  
  226. \makeNewKeyword{\nil}{nil}
  227. \makeNewKeyword{\True}{true}
  228. \makeNewKeyword{\true}{true}
  229. \makeNewKeyword{\False}{false}
  230. \makeNewKeyword{\false}{false}
  231. \makeNewKeyword{\rem}{ rem }
  232.  
  233. \def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}
  234.  
  235. %----------------------------------------------------------------
  236. %
  237. %       monadic operator creation
  238. %
  239. \def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}
  240.  
  241. %----------------------------------------------------------------
  242. %
  243. %       primitive numeric types
  244. %
  245. % use the AMS fonts for these if possible
  246.  
  247. \ifams@
  248.   \DeclareMathSymbol{\Bool} {\mathord}{AMSb}{"42}   % Booleans
  249.   \DeclareMathSymbol{\Nat}  {\mathord}{AMSb}{"4E}   % Natural numbers
  250.   \def\Nati{\Nat_1}             % Positive natural numbers
  251.   \DeclareMathSymbol{\Int}  {\mathord}{AMSb}{"5A}   % Integers
  252.   \DeclareMathSymbol{\Real} {\mathord}{AMSb}{"52}   % Reals
  253.   \DeclareMathSymbol{\Rat}  {\mathord}{AMSb}{"51}   % Rationals
  254. \else
  255.   \def\Bool{\nfss@text{\bfseries B\/}}
  256.   \def\Nat{\nfss@text{\bfseries N\/}}
  257.   \def\Nati{\hbox{$\nfss@text{\bfseries N}_1$}}
  258.   \def\Int{\nfss@text{\bfseries Z\/}}
  259.   \def\Real{\nfss@text{\bfseries R\/}}
  260.   \def\Rat{\nfss@text{\bfseries Q\/}}
  261. \fi
  262. \let\Natone=\Nati % just for an alternative
  263.  
  264. %----------------------------------------------------------------
  265. %
  266. %       Operations
  267. %
  268. % The op environment.  Within op you can specify args,
  269. % result, etc. which are gathered into registers, and output when the
  270. % op env. ends.
  271. %
  272. % The optional argument is the operation name
  273.  
  274. % shorthand for an operation on its own: the vdmop env.
  275. \def\vdmop{\vdm\op} \def\endvdmop{\endop\endvdm}
  276.  
  277. % registers constructed within an op environment
  278. \newtoks\@operationName
  279. \newbox\@operationNameBox
  280. \newif\ifArgumentListEncountered@
  281. \newtoks\@argumentListTokens
  282. \newtoks\@resultNameAndTypeTokens
  283. \newbox\@externalsBox
  284. \newbox\@preConditionBox
  285. \newbox\@postConditionBox
  286. \newbox\@errConditionBox
  287.  
  288. \def\op{% clear temporaries, deal with optional arg
  289.         \setbox\@operationNameBox=\hbox{}%
  290.         \@argumentListTokens={}\ArgumentListEncountered@false
  291.         \@resultNameAndTypeTokens={}%
  292.         \setbox\@externalsBox=\box\voidb@x
  293.         \setbox\@preConditionBox=\box\voidb@x
  294.         \setbox\@postConditionBox=\box\voidb@x
  295.         \par\preOperationHook
  296.         \vskip\preOperationSkip
  297.         \@beginVerticalVDM
  298.         \@ifnextchar [{\@opname}{}}
  299.  
  300. % breaking parameters
  301. \newcount\preOperationPenalty \preOperationPenalty=0
  302. \newcount\preExternalPenalty \preExternalPenalty=2000
  303. \newcount\prePreConditionPenalty \prePreConditionPenalty=800
  304. \newcount\prePostConditionPenalty \prePostConditionPenalty=500
  305. \newcount\preErrConditionPenalty \preErrConditionPenalty=500
  306. \newcount\postOperationPenalty \postOperationPenalty=-500
  307.  
  308. % gaps between bits of operations
  309. \newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
  310. \newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
  311. \newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
  312. \newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
  313. \newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
  314. \newskip\preErrConditionSkip \preErrConditionSkip=.5ex plus .2ex minus .2ex
  315.  
  316. \def\endop{% make up operation
  317.         % IMPORTANT---don't remove the vskips in this macro
  318.         % if you don't want one, set it to 0pt
  319.         \vskip 0pt
  320.         \@setOperationHeader
  321.         \betweenHeaderAndExternalsHook
  322.         \vskip\postHeaderSkip
  323.         \ifvoid\@externalsBox
  324.               \betweenExternalsAndPreConditionHook
  325.         \else \moveright\VDMindent\box\@externalsBox
  326.               \betweenExternalsAndPreConditionHook
  327.               \vskip\postExternalsSkip
  328.         \fi
  329.         \ifvoid\@preConditionBox
  330.               \betweenPreAndPostConditionHook
  331.         \else \moveright\VDMindent\box\@preConditionBox
  332.               \betweenPreAndPostConditionHook
  333.               \vskip\postPreConditionSkip
  334.         \fi
  335.         \ifvoid\@postConditionBox
  336.               \betweenPostAndErrHook
  337.         \else \moveright\VDMindent\box\@postConditionBox
  338.               \betweenPostAndErrConditionHook
  339.         \fi
  340.         \ifvoid\@errConditionBox
  341.         \else \vskip\preErrConditionSkip
  342.               \moveright\VDMindent\box\@errConditionBox
  343.         \fi
  344.         \postOperationHook
  345.         \vskip\postOperationSkip}
  346.  
  347. % hooks for user-defined expansion
  348. % TeX is in outer vertical mode when these are called.
  349. % ALWAYS leave TeX in vertical mode after these macros have been called
  350. \def\preOperationHook{\penalty\preOperationPenalty }
  351. \def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
  352. \def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
  353. \def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
  354. \def\betweenPostAndErrConditionHook{\penalty\preErrConditionPenalty }
  355. \def\postOperationHook{\penalty\postOperationPenalty }
  356.  
  357. % combine the operation name, argument list and result
  358. \def\@setOperationHeader{%
  359.         \moveright\VDMindent\vtop{%
  360.                 \ifArgumentListEncountered@
  361.                         \setbox\@operationNameBox=%
  362.                                 \hbox{\unhbox\@operationNameBox$($}\fi
  363.                 \hangindent=\wd\@operationNameBox \hangafter=1
  364.                 \noindent\kern-.05em\box\@operationNameBox
  365.                 \@beginHorizontalVDM
  366.                 \ifArgumentListEncountered@\the\@argumentListTokens)\fi
  367.                 \ \the\@resultNameAndTypeTokens
  368.                 \@endHorizontalVDM}}
  369.  
  370. % set the operation name
  371. % \opname{name-of-operation}
  372. \def\opname#1{\@opname[#1]}
  373. \def\@opname[#1]{\@operationName={#1}%
  374.   \global\setbox\@operationNameBox=\hbox{$\relax#1$\ }}
  375.  
  376. % set up the argument list
  377. % \args{ argument \\ argument \\ argument... } where \\ forces a line break
  378. % This is also used in the fn environment
  379. \def\args{\global\ArgumentListEncountered@true \global\@argumentListTokens=}
  380.  
  381. % result name and type
  382. \def\res{\global\@resultNameAndTypeTokens=}
  383.  
  384. % externals list
  385. %
  386. % An external list could be either very long or very short, so we provide
  387. % two forms.  One is the short \ext{..} command, the other is the externals
  388. % environment.
  389. % Externals are always separated by \\
  390. %
  391.  
  392. % we have to mess a little to get the catcode of : right
  393. \def\ext{\bgroup\@makeColonActive\@ext}
  394. \def\@ext#1{\externals#1\endexternals\egroup}
  395.  
  396. \def\externals{\global\setbox\@externalsBox=%
  397.         \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
  398. \def\endexternals{\@endIndentedPara{\@endAlignment}}
  399.  
  400. \def\@setUpExternals{\@makeColonActive\@changeLineSeparator\@beginAlignment}
  401.  
  402. % more catcode trickery for :
  403. {\catcode`\:=\active
  404.  \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}
  405.  
  406. % the \expandafters are necessary because TeX doesn't expand
  407. % \halign specs when scanning for # and &
  408. \def\@beginAlignment{\expandafter\halign\expandafter\bgroup
  409.         \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
  410. \def\@endAlignment{\crcr\egroup}
  411.  
  412. % the user can decide on the exact alignment of the field names
  413. \newtoks\@extAlign
  414. \def\leftExternals{\@extAlign={$##$\hfil}}
  415. \def\rightExternals{\@extAlign={\hfil$##$}}
  416. \leftExternals
  417.  
  418. \makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }
  419.  
  420. % pre-condition, post-condition and err-condition
  421. %
  422. % once again we provide short forms \pre, \post, \err and environments
  423. % precond, postcond and errcond
  424. \def\pre#1{\precond#1\endprecond}
  425. \def\precond{\global\setbox\@preConditionBox=%
  426.         \@beginMathIndentedPara{\hsize}{pre }}
  427. \def\endprecond{\@endMathIndentedPara}
  428.  
  429. \def\post#1{\postcond#1\endpostcond}
  430. \def\postcond{\global\setbox\@postConditionBox=%
  431.         \@beginMathIndentedPara{\hsize}{post }}
  432. \def\endpostcond{\@endMathIndentedPara}
  433.  
  434. \def\err#1{\errcond#1\enderrcond}
  435. \def\errcond{\global\setbox\@errConditionBox=%
  436.         \@beginMathIndentedPara{\hsize}{errs }}
  437. \def\enderrcond{\@endMathIndentedPara}
  438.  
  439.  
  440. %----------------------------------------------------------------
  441. %
  442. %       Box man\oe uvres
  443. %
  444. % Here's where all the tricky box manipulation commands go
  445. %
  446. % \@beginIndentedPara begins construction of a \hbox of width #1
  447. % which contains keyword #2 to the left of a para in a vtop.
  448. % #3 is evaluated within the inner vtop.
  449. % endIndentedPara closes the box off; its arg. is evaluated just
  450. % before closing the box.
  451. %
  452. \def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
  453.         \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
  454. \def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
  455.  
  456. % \@beginMathIndentedPara places the para in vdm mode
  457. \def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
  458.         {\@beginHorizontalVDM}}
  459. \def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontalVDM}}
  460.  
  461. % \@belowAndIndent#1#2 places #2 in a vbox below and to the right of #1
  462. \def\@belowAndIndent#1#2{#1\hfil\break
  463.         \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  464.  
  465. % \@mathIndentedPara does the whole thing
  466. \def\@mathIndentedPara#1#2#3{\@beginMathIndentedPara{#1}{#2}#3%
  467.         \@endMathIndentedPara}
  468. %----------------------------------------------------------------
  469. %
  470. %       Constructions
  471. %
  472. % Here are all the standard constructions.
  473. % The only tricky one is \cases.
  474. % Those that construct a box must be made to make that box of 0 width,
  475. % and force a line break immediately afterwards.
  476.  
  477. % \If mm-exp \Then mm-exp \Else mm-exp \Fi
  478. % multi-line indented if-then-else
  479. %
  480. \def\If#1\Then#2\Else#3\Fi{\vtop{%
  481.         \@mathIndentedPara{0pt}{if }{#1}%
  482.         \@mathIndentedPara{0pt}{then }{#2}%
  483.         \@mathIndentedPara{0pt}{else }{#3}}}
  484.  
  485. % \SIf mm-exp \Then mm-exp \Else mm-exp \Fi
  486. % single line if-then-else
  487. \def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  488.         \kw{if }\nobreak#1\penalty0\hskip 0.5em
  489.         \kw{then }\nobreak#2\penalty-100\hskip 0.5em % break here OK
  490.         \kw{else }\nobreak#3\@endHorizontalVDM}\hss}}
  491.  
  492. % \Let mm-exp \In mm-exp2
  493. % multi-line let..in ; mm-exp2 is `curried'
  494. \def\Let#1\In{\vtop{%
  495.         \@mathIndentedPara{0pt}{let }{#1\hskip 0.5em\kw{in}}}\hfil\break}
  496.  
  497. % \SLet mm-exp \In mm-exp
  498. % single-line let..in
  499. \def\SLet#1\In#2{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  500.         \kw{let }\nobreak#1\hskip 0.5em
  501.         \kw{in }\penalty-100 #2\@endHorizontalVDM}\hss}}
  502.  
  503. % multi-line cases
  504. %
  505. % \Cases{ selecting-mm-exp }
  506. % from-case1 & to-case1 \\
  507. % from-case2 & to-case2 \\
  508. %           ...
  509. % from-casen & to-casen
  510. % \Otherwise{ mm-exp }
  511. % \Endcases[optional text for the rest of the line]
  512.  
  513. \newif\ifOtherwiseEncountered@
  514. \newtoks\@OtherwiseTokens
  515.  
  516. \def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
  517.                 \@mathIndentedPara{\hsize}{cases }{\strut
  518.                         #1\hskip 0.5em\strut\kw{of}}%
  519.                 \bgroup % we might be in a nested case, so we have to
  520.                         % save the \Otherwise bits we might lose
  521.                 \OtherwiseEncountered@false \@changeLineSeparator
  522.                 \@beginCasesAlignment}
  523.  
  524. % the user can decide on the exact alignment
  525. \newtoks\@casesDef
  526. \def\leftCases{\@casesDef={$##$\hfil}}
  527. \def\rightCases{\@casesDef={\hfil$##$}}
  528. \rightCases
  529.  
  530. % the \expandafters are necessary because TeX doesn't expand
  531. % \halign specs when scanning for # and &
  532. \def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
  533.         \the\@casesDef&$\,\rightarrow##$\hfil\cr}
  534.  
  535. \def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
  536. \let\Others=\Otherwise
  537.  
  538. \def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
  539. \def\@endCasesAlignment{\crcr\egroup}
  540. \def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
  541.         \@mathIndentedPara{\hsize}{others }{%
  542.                 \strut\the\@OtherwiseTokens\strut}
  543.         \fi}
  544.  
  545. % must test for the optional arg to follow the end
  546. \def\@setEndcases{\noindent
  547.         \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
  548. \def\@unbracket[#1]{$#1$\@finalCaseEnd}
  549. \def\@finalCaseEnd{\egroup\hss\egroup}%\hfil\break
  550.  
  551. %----------------------------------------------------------------
  552. %
  553. %       special symbols
  554.  
  555. % defined as
  556. \def\DEF{\raise.5ex
  557.         \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle
  558.  
  559.  
  560. % cross product
  561. \let\x=\times
  562.  
  563. %       logical connectives
  564. %
  565. \def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
  566.         \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
  567. \let\iff=\Iff
  568. \def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
  569.         \mskip 6mu plus 2mu minus 1mu}
  570. \let\implies=\Implies
  571. % see changeOtherMathcodes for \Or
  572. \let\And=\land
  573. \let\@and=\and
  574. \def\and{\ifmmode\And\else\@and\fi}
  575. %  use \neg for logical not, or
  576. \def\Not{\neg\,}
  577.  
  578. %       quantification
  579. %
  580.  
  581. \DeclareMathSymbol{\Exists}   {\mathord}{symbols}{"39}
  582. \DeclareMathSymbol{\Forall}   {\mathord}{symbols}{"38}
  583. \DeclareMathSymbol{\suchthat} {\mathbin}{symbols}{"01}
  584.  
  585. \def\exists{\@ifstar{\@splitExists}{\@normalExists}}
  586. \ifams@
  587.   \DeclareMathSymbol{\@nexists} {\mathop}{AMSb}{"40}
  588.                % crossed out existential quantifier
  589. \else
  590.   \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
  591. \fi
  592. \def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
  593. \def\forall{\@ifstar{\@splitForall}{\@normalForall}}
  594. \def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
  595. \def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}
  596.  
  597. \def\@normalExists#1#2{{\Exists#1}\suchthat #2}
  598. \def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
  599. \def\@normalForall#1#2{{\Forall#1}\suchthat #2}
  600. \def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
  601. \def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}
  602.  
  603. \def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
  604. \def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
  605. \def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
  606. \def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
  607. \def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
  608. %
  609. %       sequents
  610. %
  611. \let\Tstlp=\vdash
  612. %
  613. \def\sequent{\@ifstar{\@splitSequent}{\@normalSequent}}
  614. \def\@normalSequent#1#2{{#1}\:\Tstlp\: #2}
  615. \def\@splitSequent#1{\@belowAndIndent{#1\;\Tstlp}}
  616.  
  617. %
  618. %       strachey brackets
  619. %
  620. % (see TeXbook, p.437)
  621. \def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
  622.  
  623. %       function composition
  624. %
  625. \let\compf=\circ
  626.  
  627. %----------------------------------------------------------------
  628. %
  629. %       function environment
  630. %
  631. % This environment is similar to the op environment, but is used for
  632. % function definition.
  633. %
  634. % The mandatory first parameter is the name of the function, the
  635. % second is the argument list.
  636. %
  637. % The *-form simply doesn't force the parentheses round the argument list
  638.  
  639. \def\fn{\parens@true\@beginVDMfunction}
  640. \@namedef{fn*}{\parens@false\@beginVDMfunction}
  641. \@namedef{endfn*}{\endfn}
  642.  
  643. % short form
  644. \def\vdmfn{\vdm\parens@true \@beginVDMfunction}
  645. \def\endvdmfn{\endfn\endvdm}
  646. \@namedef{vdmfn*}{\vdm\parens@false \@beginVDMfunction}
  647. \@namedef{endvdmfn*}{\endfn\endvdm}
  648.  
  649. % registers used within the fn environment
  650. \newtoks\@fnName
  651. \newbox\@fnNameBox
  652. \newif\ifsignatureEncountered@
  653. \newtoks\@signatureTokens
  654. \newbox\@fnDefnBox
  655. \newif\ifparens@
  656.  
  657. \def\@beginVDMfunction#1#2{%
  658.         \@fnName={#1}%
  659.         \setbox\@fnNameBox=\hbox{$#1$}%
  660.         \setbox\@preConditionBox=\box\voidb@x % for people who want to do
  661.         \setbox\@postConditionBox=\box\voidb@x% implicit defns
  662.         \@signatureTokens={}\signatureEncountered@false
  663.         \ifparens@
  664.                 \@argumentListTokens={(#2)}%
  665.         \else
  666.                 \@argumentListTokens={#2}%
  667.         \fi
  668.         \par\preFunctionHook
  669.         \vskip\preFunctionSkip
  670.         \@beginVerticalVDM
  671.         \@beginFnDefn}
  672.  
  673. % read in a signature
  674. \def\signature{\global\signatureEncountered@true \global\@signatureTokens=}
  675.  
  676. \def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
  677.         \hangindent=2em \hangafter=1 \@beginHorizontalVDM
  678.         \advance\hsize by-2em % this fools vboxes within the
  679.         % function body about the hanging indent...yuk.
  680.         % If you change the size of the indent, change the
  681.         % corresponding line in \endfn.
  682.         \copy\@fnNameBox \the\@argumentListTokens
  683.         \quad\DEF\penalty-100\quad }
  684.  
  685. \newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
  686. \newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
  687. \newskip\betweenSignatureAndBodySkip
  688. \betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
  689. \newskip\betweenFunctionAndPreSkip
  690. \betweenFunctionAndPreSkip=1.2ex plus .3ex minus .2ex
  691.  
  692. \def\endfn{%
  693.         \advance\hsize by 2em% matches the dirty \advance in \@beginFnDefn
  694.         \@endHorizontalVDM
  695.         \egroup  % this ends the vtop we started in \@beginFnDefn
  696.         \ifsignatureEncountered@
  697.                 \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
  698.                 \dimen255=\wd0 \noindent \box0
  699.                 \vtop{\advance\hsize by-\dimen255 \@beginHorizontalVDM
  700.                         \the\@signatureTokens \@endHorizontalVDM}\par
  701.                 \betweenSignatureAndBodyHook
  702.                 \vskip\betweenSignatureAndBodySkip
  703.         \fi
  704.         \moveright\VDMindent\box\@fnDefnBox\,
  705.         \ifvoid\@preConditionBox
  706.               \betweenPreAndPostConditionHook
  707.               \vskip\postFunctionSkip
  708.         \else \betweenFunctionAndPreHook
  709.               \vskip\betweenFunctionAndPreSkip
  710.               \moveright\VDMindent\box\@preConditionBox
  711.               \betweenPreAndPostConditionHook
  712.               \vskip\postPreConditionSkip
  713.         \fi
  714.         \ifvoid\@postConditionBox
  715.               \postFunctionHook
  716.         \else \moveright\VDMindent\box\@postConditionBox
  717.               \postFunctionHook
  718.               \vskip\postOperationSkip
  719.         \fi}
  720.  
  721. \newcount\preFunctionPenalty \preFunctionPenalty=0
  722. \newcount\betweenSignatureAndBodyPenalty
  723.  \betweenSignatureAndBodyPenalty=10000
  724. \newcount\betweenFunctionAndPrePenalty \betweenFunctionAndPrePenalty=1000
  725. \newcount\postFunctionPenalty \postFunctionPenalty=-500
  726.  
  727. % These are called in outer vertical mode---they must also exit in this mode
  728. \def\preFunctionHook{\penalty\preFunctionPenalty }
  729. \def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
  730. \def\betweenFunctionAndPreHook{\penalty\betweenFunctionAndPrePenalty }
  731. \def\postFunctionHook{\penalty\postFunctionPenalty }
  732.  
  733. %       other function-related things
  734. %
  735.  
  736. % function arrow
  737. \def\to{\penalty-100\rightarrow}
  738.  
  739. % explicit lamdba function
  740. \def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
  741. \def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
  742. \def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
  743.         {\lambda#1}\suchthat\hfil\break
  744.         \@mathIndentedPara{\hsize}{\qquad}{#2}}
  745.  
  746. %----------------------------------------------------------------
  747. %
  748. %       Optional fields
  749. %
  750. \def\Opt#1{\big[#1\big]}
  751.  
  752.  
  753. %----------------------------------------------------------------
  754. %
  755. %       Sets
  756.  
  757. % new set type
  758. \def\setof#1{#1-\kw{set}}
  759.  
  760. % set enumeration
  761. \def\set#1{\{#1\}}
  762.  
  763. % empty set
  764. \def\emptyset{\{\,\}}
  765.  
  766. % usual LaTeX operators apply: \in \notin \subset \subseteq
  767. \let\inter=\cap \let\intersection=\inter
  768. \let\Inter=\bigcap \let\Intersection=\Inter
  769. \let\union=\cup
  770. \let\Union=\bigcup
  771.  
  772. \mathchardef\minus="2200
  773.  
  774. \def\diff{\minus} \let\difference=\diff
  775.  
  776. \newMonadicOperator{\card}{card}
  777. \newMonadicOperator{\Min}{min}
  778. \newMonadicOperator{\Max}{max}
  779. \newMonadicOperator{\abs}{abs}
  780.  
  781. %----------------------------------------------------------------
  782. %
  783. %       Map type
  784.  
  785. % new map type
  786. \def\mapof#1#2{#1\buildrel m\over\longrightarrow#2}
  787.  
  788. % one-one map
  789. \def\mapinto#1#2{#1\buildrel m\over\longleftrightarrow#2}
  790.  
  791. % map enumeration
  792. \def\map#1{\{#1\}}
  793.  
  794. % empty map
  795. \def\emptymap{\{\,\}}
  796.  
  797. %       map operators
  798. %
  799. % use \mapsto for |->
  800. % overwrite
  801. \def\owr{\dagger}
  802.  
  803. \let\dres=\lhd
  804. \let\rres=\rhd
  805.  
  806.  
  807. % domain subtraction
  808. \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  809.         \lower.1ex\hbox{$\dres$}$}}}
  810.  
  811. % range subtraction
  812. \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  813.         \lower.1ex\hbox{$\rres$}$}}}
  814.  
  815. \newMonadicOperator{\dom}{dom}
  816. \newMonadicOperator{\rng}{rng}
  817. \newMonadicOperator{\merge}{merge}
  818.  
  819. %----------------------------------------------------------------
  820. %
  821. %       Sequences
  822. %
  823.  
  824. % new type
  825. \def\seqof#1{#1^*}
  826.  
  827. % non-empty sequence
  828. \def\neseqof#1{#1^+}
  829.  
  830. % enumeration
  831. \def\seq#1{[#1]}
  832.  
  833. % empty sequence
  834. \def\emptyseq{[\,]}
  835.  
  836. \newMonadicOperator{\len}{len}
  837. \newMonadicOperator{\hd}{hd}
  838. \newMonadicOperator{\tl}{tl}
  839. \newMonadicOperator{\elems}{elems}
  840. \newMonadicOperator{\inds}{inds}
  841. \def\cons#1{\kw{cons}\nobreak(#1)}
  842.  
  843. % sequence concatenation
  844.  
  845. \DeclareMathSymbol{\@sc@nc} {\mathbin}{AMSb}{"79}
  846.  
  847. \ifams@
  848.   \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\@sc@nc$}}}}
  849. \else
  850.   % this is truly yukky
  851.   \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
  852.         \raise0.2ex\hbox{\it\char"12}}}}
  853. \fi
  854.  
  855. % distributed concatenation
  856. \newMonadicOperator{\Conc}{dconc}
  857.  
  858. %----------------------------------------------------------------
  859. %
  860. %       type equation
  861. %
  862. \newtoks\@typeName
  863. \def\type#1#2{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  864.         \@beginVerticalVDM
  865.         \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
  866.                 \@endHorizontalVDM}
  867.         \postTypeHook \vskip\postTypeSkip}}
  868.  
  869. % restricted type (has invariant)
  870. \def\rtype#1#2#3{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  871.         \@beginVerticalVDM
  872.         \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
  873.                 \@endHorizontalVDM}
  874.         \vskip\betweenTypeAndInvSkip
  875.         \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
  876.         \postTypeHook \vskip\postTypeSkip}}
  877.  
  878. % initialised type
  879. \def\ritype#1#2#3#4{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  880.         \@beginVerticalVDM
  881.         \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
  882.                 \@endHorizontalVDM}
  883.         \vskip\betweenTypeAndInvSkip
  884.         \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
  885.         \vskip\betweenInvAndInitSkip
  886.         \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{#4}%
  887.         \postTypeHook \vskip\postTypeSkip}}
  888.  
  889. \def\preTypeHook{} \def\postTypeHook{}
  890. \newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
  891. \newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
  892. \newskip\betweenTypeAndInvSkip
  893.   \betweenTypeAndInvSkip=.5ex plus .3ex minus .2ex
  894. \newskip\betweenInvAndInitSkip
  895.   \betweenInvAndInitSkip=.5ex plus .3ex minus .2ex
  896.  
  897. %----------------------------------------------------------------
  898. %
  899. %       Composite Objects
  900. %
  901.  
  902. % literal composition; we have a compose and a composite env.
  903.  
  904. % single line compose
  905. \@namedef{composite*}#1{\kw{compose }$\relax#1\relax$\kw{ of }$\relax}
  906. \@namedef{endcomposite*}{\relax$\kw{ end}}
  907.  
  908. % multiple line version
  909. \def\composite#1{\bgroup\vskip\preCompositeSkip
  910.     \@beginVerticalVDM
  911.     \moveright\VDMindent\vtop\bgroup
  912.         \@beginHorizontalVDM
  913.         \kw{compose }#1\kw{ of}%
  914.         \@endHorizontalVDM
  915.         \@makeColonActive\@changeLineSeparator
  916.         \expandafter\halign\expandafter\bgroup\expandafter\qquad
  917.                 \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  918. \def\endcomposite{\crcr\egroup % closes \halign
  919.         \kw{end}\egroup % ends the \vtop
  920.         \vskip\postCompositeSkip\egroup}
  921.  
  922. \def\scompose#1#2{\@nameuse{composite*}{#1}{#2}\@nameuse{endcomposite*}}
  923.  
  924. \newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
  925. \newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex
  926.  
  927. % record composites; likewise we have a short and a long form
  928. \newtoks\@recordName
  929.  
  930. \def\record#1{%
  931.   \InvEncountered@false \InitEncountered@false
  932.   \@invTokens={}\@initTokens={}
  933.   \@recordName{#1}
  934.   \par\preRecordHook
  935.   \vskip\preRecordSkip
  936.   \@beginVerticalVDM
  937.   \moveright\VDMindent\hbox\bgroup
  938.           \setbox0=\hbox{$#1$\enspace::\enspace}%
  939.           \@makeColonActive\@changeLineSeparator
  940.           \advance\hsize by-\wd0 \box0
  941.           \@restoreMargins
  942.           %
  943.           % the \expandafters are necessary because TeX doesn't expand
  944.           % \halign specs when scanning for # and &
  945.           \vtop\bgroup\expandafter\halign\expandafter\bgroup
  946.                   \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  947.  
  948. \def\endrecord{\crcr\egroup% closes halign
  949.         \egroup% closes vtop
  950.         \egroup% closes hbox
  951.   \ifInvEncountered@
  952.         \betweenRecordAndInvHook
  953.         \vskip\betweenRecordAndInvSkip
  954.         \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{%
  955.                 \the\@invTokens}
  956.   \fi
  957.   \ifInitEncountered@
  958.         \betweenInvAndInitHook
  959.         \vskip\betweenInvAndInitSkip
  960.         \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{%
  961.                 \the\@initTokens}
  962.   \fi
  963.   \par\postRecordHook
  964.   \vskip\postRecordSkip}
  965.  
  966. \def\inv{\global\InvEncountered@true \global\@invTokens=}
  967. \def\init{\global\InitEncountered@true \global\@initTokens=}
  968.  
  969. \newif\ifInvEncountered@
  970. \newif\ifInitEncountered@
  971. \newtoks\@invTokens
  972. \newtoks\@initTokens
  973. \def\betweenRecordAndInvHook{}
  974. \def\betweenInvAndInitHook{}
  975. \newskip\betweenRecordAndInvSkip
  976.   \betweenRecordAndInvSkip=0.5ex plus 0.2ex minus 0.1ex
  977. \newskip\betweenInvAndInitSkip
  978.   \betweenInvAndInitSkip=0.5ex plus 0.2ex minus 0.1ex
  979.  
  980. % the user can decide on the exact alignment of the field names
  981. \newtoks\@recordAlign
  982. \def\leftRecord{\@recordAlign={$##$\hfil}}
  983. \def\rightRecord{\@recordAlign={\hfil$##$}}
  984. \rightRecord
  985.  
  986. % more catcode trickery
  987. \def\defrecord{\bgroup\@makeColonActive\@defrecord}
  988. \def\@defrecord#1#2{\record{#1}#2\endrecord\egroup}
  989.  
  990. \newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
  991. \newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
  992. \newcount\preRecordPenalty \preRecordPenalty=0
  993. \newcount\postRecordPenalty \postRecordPenalty=-100
  994. \def\preRecordHook{\penalty\preRecordPenalty }
  995. \def\postRecordHook{\penalty\postRecordPenalty }
  996.  
  997. % \chg: mu function on composites
  998. \def\chg#1#2#3{\mu(#1,#2\mapsto#3)}
  999.  
  1000. %----------------------------------------------------------------
  1001. %
  1002. %       Hooks
  1003. %
  1004. % hooked identifiers --- these are taken from the TeXbook, p.357, 359
  1005. \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  1006.   \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
  1007.   \mkern-6mu \mathord\minus$}  % p.357, \leftarrowfill
  1008.  
  1009. \def\overleftharpoonup#1{{%
  1010.   \boxmaxdepth=\maxdimen % this fixes Lamport's figures, but isn't necessary
  1011.                          % for versions after 15 Dec 87
  1012.   \vbox{\ialign{##\crcr % p.359, \overleftarrow
  1013.     \leftharpoonupfill\crcr\noalign{\kern-\p@\nointerlineskip}
  1014.     $\hfil\displaystyle{#1}\hfil$\crcr}}}}
  1015.  
  1016. \let\hook=\overleftharpoonup  % c'est simple comme bonjour
  1017.  
  1018. %-----------------------------------------------------------------
  1019. %
  1020. %       General formula environment, a bit like \[ \] but is
  1021. %       indented to \VDMindent and will take \\
  1022. %
  1023. %
  1024. \def\form#1{\formula #1\endformula}
  1025.  
  1026. \def\formula{\par\preFormulaHook
  1027.         \vskip\preFormulaSkip
  1028.         \@beginVerticalVDM
  1029.         \bgroup
  1030.         \moveright\VDMindent\vtop\bgroup\@beginHorizontalVDM}
  1031. \def\endformula{\@endHorizontalVDM\egroup % ends the vtop
  1032.         \egroup % ends the overall group
  1033.         \par\postFormulaHook
  1034.         \vskip\postFormulaSkip}
  1035.  
  1036. \newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
  1037. \newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
  1038. \newcount\preFormulaPenalty \preFormulaPenalty=0
  1039. \newcount\postFormulaPenalty \postFormulaPenalty=-100
  1040. \def\preFormulaHook{\penalty\preFormulaPenalty }
  1041. \def\postFormulaHook{\penalty\postFormulaPenalty }
  1042.  
  1043. %----------------------------------------------------------------
  1044. %
  1045. %       Formula within a box, when width is unknown
  1046. %
  1047. %       equivalent to \parbox[t]{\hsize}{\@beginHorizontalVDM
  1048. %               ...\@endHorizontalVDM}
  1049. %
  1050. \def\formbox{\vtop\bgroup\@beginHorizontalVDM}
  1051. \def\endformbox{\strut\@endHorizontalVDM\egroup}
  1052.  
  1053. %----------------------------------------------------------------
  1054. %
  1055. %       special font for constants
  1056. %
  1057. \def\constantFont{\sc}
  1058. \def\const#1{\hbox{\constantFont{#1}\/}}
  1059.  
  1060. %----------------------------------------------------------------
  1061. %
  1062. %       line break and indent
  1063. %
  1064. \def\T#1{\\\hbox to #1em{}}
  1065.  
  1066. %----------------------------------------------------------------
  1067. %
  1068. %       line break and push line after to RHS
  1069. %
  1070. \def\R{\\\hspace*{\fill}}
  1071.  
  1072. %----------------------------------------------------------------
  1073. %
  1074. %       Proofs
  1075. %
  1076. % a proof environment for typesetting proofs in the "natural
  1077. % deduction" style.
  1078.  
  1079. \newdimen\ProofIndent \ProofIndent=\VDMindent
  1080. \newdimen\ProofNumberWidth \ProofNumberWidth=\parindent
  1081.  
  1082. \def\proof{\par\preProofHook
  1083.         \vskip\preProofSkip
  1084.         \let\&=\@proofLine
  1085.         \moveright\ProofIndent\vtop\bgroup
  1086.                 \@indentLevel=1
  1087.                 \advance\linewidth by-\ProofIndent
  1088.                 \begin{tabbing}%
  1089.                 \hbox to\ProofNumberWidth{}\=\kill}     % template line
  1090. \def\endproof{\end{tabbing}\advance\linewidth by\ProofIndent
  1091.         \egroup % ends the \vtop
  1092.         \par\postProofHook
  1093.         \vskip\postProofSkip}
  1094.  
  1095. \newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
  1096. \newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex
  1097.  
  1098. \newcount\preProofPenalty \preProofPenalty=-100
  1099. \newcount\postProofPenalty \postProofPenalty=0
  1100. \def\preProofHook{\penalty\preProofPenalty }
  1101. \def\postProofHook{\penalty\postProofPenalty }
  1102.  
  1103. \def\From{\@indentProof\kw{from }\=%
  1104.         \global\advance\@indentLevel by 1
  1105.         \@enterMathMode}
  1106. \def\Infer{\global\advance\@indentLevel by-1
  1107.         \@indentProof\kw{infer }\@enterMathMode}
  1108. \def\@proofLine{\@indentProof\@enterMathMode}
  1109. \def\by{\`}
  1110.  
  1111. \newcount\@indentLevel
  1112. \newcount\@indentCount
  1113. \def\@indentProof{% do \>, \@indentLevel times
  1114.         \global\@indentCount=\@indentLevel
  1115.         \@gloop \>\global\advance\@indentCount by-1
  1116.         \ifnum\@indentCount>0
  1117.         \repeat}
  1118.  
  1119. % need special loop macros that works in across boxes
  1120. \def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
  1121. \def\@giterate{\@body \global\let\@gloopNext=\@giterate
  1122.         \else \global\let\@gloopNext=\relax \fi \@gloopNext}
  1123.  
  1124. % this enters math mode and sets the LaTeX macros \@stopfield up
  1125. % to exit math mode
  1126. \def\@enterMathMode{\def\@stopfield{$\egroup}$}
  1127.  
  1128. %----------------------------------------------------------------
  1129. \def\VDMauthor{M.Wolczko,
  1130. CS Dept.,
  1131. Univ. of Manchester, UK.
  1132. mario@cs.man.ac.uk
  1133. uknet!man.cs!mario}
  1134.  
  1135. \def\VDMversion{vdm3.0}
  1136.  
  1137. \typeout{BSI VDM style option <9 Jun 1992>}
  1138. %----------------------------------------------------------------
  1139. %
  1140. %       Global changes
  1141. %
  1142. % All things that have to be invoked before the user's stuff appears
  1143. % should go here.
  1144. %
  1145. % by default the math spacing and changes to @ and _ apply everywhere
  1146. \@changeOtherMathcodes \@changeGlobalCatcodes
  1147. %
  1148. %-------------------the end--------------------------------------
  1149. \endinput
  1150. %
  1151. %       Summary of penalties
  1152. %
  1153. %       Penalties in vertical mode
  1154. %
  1155. % \preOperationPenalty          before an op begins
  1156. % \preExternalPenalty           between the header and externals of an op
  1157. % \prePreConditionPenalty       before the precondition
  1158. % \prePostConditionPenalty      before the postcondition
  1159. % \postOperationPenalty         at the end of an op
  1160. %
  1161. % \preFunctionPenalty           before a fn begins
  1162. % \betweenSignatureAndBodyPenalty -guess
  1163. % \postFunctionPenalty          after a fn ends
  1164. %
  1165. % \preRecordPenalty             before a record
  1166. % \postRecordPenalty            after a record
  1167. %
  1168. %       etc for formula, proof
  1169. %
  1170. %       Penalties in horizontal mode in boxes
  1171. %
  1172. % \linepenalty                  101             \@raggedRight
  1173. % `if mm-exp ^ then..'          0               \SIf
  1174. % `if ... then mm-exp ^ else'   -100            \SIf
  1175. % `let mm-exp in ^ ...'         -100            \SLet
  1176. % `map mm-exp ^ to ...'         -50             \map
  1177. % ^\iff                         -50             \iff
  1178. % ^\implies                     -35             \implies
  1179. % func(args) \DEF^              -100            \begin{fn}
  1180. % \binoppenalty                 10000
  1181. % \relpenalty                   10000
  1182. % \hyphenpenalty                -100            \suchthat
  1183. % ^\to                          -100            \to
  1184. % _^                            100             \@VDMunderscore
  1185. %
  1186.